nLab natural numbers object

Redirected from "natural number object".
Natural numbers object

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

Induction

Natural numbers object

Idea

Recall that a topos is a category that behaves likes the category Set of sets.

A natural numbers object (NNO) in a topos is an object that behaves in that topos like the set \mathbb{N} of natural numbers does in Set; thus it provides a formulation of the “axiom of infinity” in structural set theory (such as ETCS). The definition is due to William Lawvere (1963).

Definition

In a topos or cartesian closed category

A natural numbers object in a topos (or any cartesian closed category) EE with terminal object 11 is

  • an object \mathbb{N} in EE

  • equipped with

  • such that for every other diagram 1qAfA1 \stackrel{q}{\to}A \stackrel{f}{\to} A there is a unique morphism u:Au : \mathbb{N} \to A such that

All this may be summed up by saying that a natural numbers object is an initial algebra for the endofunctor X1+XX \mapsto 1 + X (the functor underlying the “maybe monad”). Equivalently, it is an initial algebra for the endo-profunctor Hom E(1,=)×Hom E(,=)Hom_E(1,=) \times Hom_E(-,=).

By the universal property, the natural numbers object is unique up to isomorphism.

Proposition

Let C,DC, D be cartesian closed categories, and suppose DD has a natural numbers object (,z:1,s:)(\mathbb{N}, z: 1 \to \mathbb{N}, s: \mathbb{N} \to \mathbb{N}). If L:DCL: D \to C is a left adjoint that preserves the terminal object, then (L,Lz,Ls)(L \mathbb{N}, L z, L s) is a natural numbers object in CC.

The proof is straightforward. It follows for example that the left adjoint part f *f^\ast of a geometric morphism f *f *:EFf^\ast \dashv f_\ast: E \to F between toposes with natural numbers objects preserves the natural numbers object, and also that a Grothendieck quasitopos QQ presented by a site (C,J)(C, J) has a natural numbers object, since the reflection functor L:Set C opQL: Set^{C^{op}} \to Q preserves finite products and the terminal object in particular.

In a closed symmetric monoidal category

One could generalize the above definition of a natural numbers object to any closed symmetric monoidal category: pointed objects in a symmetric monoidal category are represented by morphisms out of the tensor unit. Thus, a natural numbers object in a closed symmetric monoidal category CC with tensor unit 11 is

  • an object \mathbb{N} in CC

  • equipped with

  • such that for every other diagram 1qAfA1 \stackrel{q}{\to}A \stackrel{f}{\to} A there is a unique morphism u:Au : \mathbb{N} \to A such that

In a category with finite products

Note that this definition actually makes sense in any category EE having finite products, such as a pretopos. However, if EE is not cartesian closed, then it is better to explicitly assume a stronger version of this definition “with parameters” (which follows automatically when EE is cartesian closed, such as when EE is a topos). What this amounts to is demanding that (,z,s)(\mathbb{N}, z, s) not only be a natural numbers object (in the above, unparametrized sense) in EE, but that also, for each object AA, this is preserved by the cofree coalgebra functor into the Kleisli category of the comonad XA×XX \mapsto A \times X (which may be thought of as the category of maps parametrized by AA). (Put another way, the finite product structure of EE gives rise to a canonical self-indexing, and we are demanding the existence of an (unparametrized) NNO within this indexed category, rather than just within the base EE).

To be explicit:

Definition

In a category with finite products, a parametrized natural numbers object is an object NN together with maps z:1Nz: 1 \to N, s:NNs: N \to N such that given any objects AA, XX and maps f:AXf: A \to X, g:XXg: X \to X, there is a unique map ϕ f,g:A×NX\phi_{f, g}: A \times N \to X making the following diagram commute:

A 1 A,z! A×N 1 A×s A×N f ϕ f,g ϕ f,g X g X\array{ A & \stackrel{\langle 1_A, z \circ !\rangle}{\to} & A \times N & \stackrel{1_A \times s}{\leftarrow} & A \times N \\ & \mathllap{f} \searrow & \downarrow \mathrlap{\phi_{f, g}} & & \downarrow \mathrlap{\phi_{f, g}} \\ & & X & \underset{g}{\leftarrow} & X }

In the internal language, commutativity of this diagram says that ϕ f,g(a,z)=f(a)\phi_{f,g}(a,z) = f(a) and ϕ f,g(a,s(n))=g(ϕ f,g(a,n))\phi_{f,g}(a,s(n)) = g(\phi_{f,g}(a,n)).

It may seem odd that AA only appears in the domain of ff and not gg. However, this simplification is inessential, and indeed we are free to add NN to the domain of gg as well:

Proposition

If (N,z,s)(N,z,s) is a parametrized natural numbers object in a category with finite products, then for any objects AA, XX with maps f:AXf:A\to X, g:A×N×XXg:A\times N\times X \to X, there is a unique map ϕ f,g:A×NX\phi_{f,g} : A\times N \to X such that, in the internal language, ϕ f,g(a,z)=f(a)\phi_{f,g}(a,z) = f(a) and ϕ f,g(a,s(n))=g(a,n,ϕ f,g(a,n))\phi_{f,g}(a,s(n)) = g(a,n,\phi_{f,g}(a,n)) for all n:Nn:N.

Proof

Let X=A×N×XX' = A\times N\times X, and define f:AXf':A\to X' by f(a)=(a,z,f(a))f'(a) = (a,z,f(a)) and g:XXg':X'\to X' by

g(a,n,x)=(a,s(n),g(a,n,x)).g'(a,n,x) = (a,s(n),g(a,n,x)).

Then the assumption gives ϕ:A×NX\phi': A\times N \to X' such that

ϕ(a,z)=f(a)=(a,z,f(a)),ϕ(a,s(n))=g(ϕ(a,n)).\phi'(a,z) = f'(a) = (a,z,f(a)), \qquad \phi'(a,s(n)) = g'(\phi'(a,n)).

The composite A×NϕXπ 1AA \times N \xrightarrow{\phi'} X' \xrightarrow{\pi_1} A satisfies

π 1ϕ(a,z)=π 1(a,z,f(a))=a,π 1ϕ(a,s(n))=π 1g(ϕ(a,n))=π 1ϕ(a,n).\pi_1 \phi'(a,z) = \pi_1(a,z,f(a)) = a, \qquad \pi_1\phi'(a,s(n)) = \pi_1 g'(\phi'(a,n)) = \pi_1 \phi'(a,n).

Thus, by the uniqueness assumption, we have π 1ϕ(a,n)=a\pi_1 \phi'(a,n) = a for all a,na,n. By a similar argument, we have π 2ϕ(a,n)=n\pi_2 \phi'(a,n) = n for all a,na,n. Therefore, ϕ(a,s(n))=(a,n,g(a,n,ϕ(a,n)))\phi'(a,s(n)) = (a,n,g(a,n,\phi'(a,n))), and hence the composite A×NϕXπ 3XA\times N \xrightarrow{\phi'} X' \xrightarrow{\pi_3} X is the desired ϕ f,g\phi_{f,g}.

The functions which are constructible out of the structure of a category with finite products and such a “parametrized NNO” are precisely the primitive recursive ones. Specifically, the unique structure-preserving functor from the free such category FF into Set yields a bijection between Hom F(1,)Hom_F(1, \mathbb{N}) and the actual natural numbers, as well as surjections from Hom F( m,)Hom_F(\mathbb{N}^m, \mathbb{N}) onto the primitive recursive functions of arity mm for each finite mm. With cartesian closure, however, this identification no longer holds, since some non-primitive recursive functions (such as the Ackermann function) become definable as well.

In this context an important class is the class of pretoposes with a parametrized NNO - the so called arithmetic pretoposes.

In a symmetric monoidal category

One could generalize the above definition of a parameterised natural numbers object to any symmetric monoidal category: pointed objects in a symmetric monoidal category are represented by morphisms out of the tensor unit. Thus,

Definition

In a symmetric monoidal category with tensor unit 11 and tensor product (A,B)AB(A, B) \mapsto A \otimes B, a parametrized natural numbers object is an object NN together with maps z:1Nz: 1 \to N, s:NNs: N \to N such that given any objects AA, XX and maps f:AXf: A \to X, g:XXg: X \to X, there is a unique map ϕ f,g:ANX\phi_{f, g}: A \otimes N \to X making the following diagram commute:

A1 1 A×z AN 1 A×s AN ρ A ϕ f,g ϕ f,g A f X g X\array{ A \otimes 1 & \stackrel{1_A \times z}{\to} & A \otimes N & \stackrel{1_A \times s}{\leftarrow} & A \otimes N \\ \mathllap{\rho_A} \downarrow & & \downarrow \mathrlap{\phi_{f, g}} & & \downarrow \mathrlap{\phi_{f, g}} \\ A & \underset{f}{\rightarrow} & X & \underset{g}{\leftarrow} & X }

where ρ A:A1A\rho_A:A \otimes 1 \cong A is the right unitor of the symmetric monoidal category CC for object AA.

In type theory

For the moment see at inductive type the section Examples - Natural numbers

Finite colimit characterization

In a topos, the natural numbers object \mathbb{N} is uniquely characterized by the following colimit conditions due to Peter Freyd:

Theorem

In a topos, a triple (,0:1,s:)(\mathbb{N}, 0: 1 \to \mathbb{N}, s: \mathbb{N} \to \mathbb{N}) is a natural numbers object if and only if

  1. The morphism (0,s):1+(0, s): 1 + \mathbb{N} \to \mathbb{N} is an isomorphism;

  2. The diagram

    1s1\mathbb{N} \stackrel{\overset{s}{\to}}{\underset{1}{\to}} \mathbb{N} \to 1

    is a coequalizer.

The necessity of the first condition holds in any category with binary coproducts and a terminal object, and the necessity of the second holds in any category whatsoever.

Proof of theorem : necessity

For a category CC with binary coproducts and 1, the natural numbers object can be equivalently described as an initial algebra structure (0,s):1+(0, s): 1 + \mathbb{N} \to \mathbb{N} for the endofunctor F(c)=1+cF(c) = 1 + c defined on CC. Then condition 1 is a special case of Lambek's theorem, that the algebra structure map of an initial algebra is an isomorphism.

As for condition 2, given f:Xf: \mathbb{N} \to X such that f=fsf = f \circ s, the claim is that ff factors as

!1xX\mathbb{N} \overset{!}{\to} 1 \overset{x}{\to} X

for some unique xx, in fact for x=f(0)x = f(0). Uniqueness is clear since !:1!: \mathbb{N} \to 1, being a retraction for 0:10: 1 \to \mathbb{N}, is epic. On the other hand, substituting either ff or f(0)!f(0) \circ ! for gg in the diagram

1 0 s f(0) g g X 1 X X\array{ 1 & \overset{0}{\to} & \mathbb{N} & \overset{s}{\to} & \mathbb{N} \\ & ^\mathllap{f(0)} \searrow & \downarrow ^g & & \downarrow ^g \\ & & X & \underset{1_X}{\to} & X }

this diagram commutes, so that f=f(0)!f = f(0) \circ ! by the uniqueness clause in the universal property for \mathbb{N}.

Proof of theorem : sufficiency

Here we just give an outline, referring to (Johnstone), section D.5.1, for full details. Let NN be an object satisfying the two colimit conditions of Freyd. First one shows (see the lemma below) that NN has no nontrivial FF-subalgebras. Next, let AA be any FF-algebra, and let i:BN×Ai: B \to N \times A be the intersection of all FF-subalgebras of N×AN \times A. One shows that π 1i:BN\pi_1 \circ i: B \to N is an (FF-algebra) isomorphism. Thus we have an FF-algebra map f:NAf: N \to A. If g:NAg: N \to A is any FF-algebra map, then the equalizer of ff and gg is an FF-subalgebra of NN, and therefore NN itself, which means f=gf = g.

Lemma

Let FF be the endofunctor F(X)=1+XF(X) = 1+X. If NN satisfies Freyd’s colimit conditions, then any FF-subalgebra of NN is the entirety of NN.

Proof

Following (Johnstone), we may as well show that the smallest FF-subalgebra NN' of NN (the internal intersection of all FF-subalgebras) is all of NN. Let SN×NS \hookrightarrow N \times N be the union of the relation R=1,s:NN×NR = \langle 1, s \rangle: N \to N \times N and its opposite, so that SS is a symmetric relation. Working in the Mitchell-Bénabou language, one may check directly that the following formula is satisfied:

x,y:N(x,yS)((xN)(yN))\forall x, y: N (\langle x, y \rangle \in S) \Rightarrow ((x \in N') \Leftrightarrow (y \in N'))

Let us say a term ww of type PNP N is SS-closed if the formula

x,y:N(x,yS)((x[w])(y[w]))\forall x, y: N (\langle x, y \rangle \in S) \Rightarrow ((x \in [w]) \Leftrightarrow (y \in [w]))

is satisfied. Now define a relation TT on NN by the subobject

{x,yN×N:w:PN(wisSclosed)((x[w])(y[w])).\{\langle x, y \rangle \in N \times N: \forall w: P N (w \; is \; S closed) \Rightarrow ((x \in [w]) \Leftrightarrow (y \in [w])).

Observe that TT is an equivalence relation that contains SS and therefore RR. It therefore contains the kernel pair of the coequalizer of 11 and ss; since this coequalizer is by assumption N1N \to 1, the kernel pair is all of N×NN \times N. Also observe that since NN' is SS-closed by definition, it is TT-closed as well, and we now conclude

x,yN:(xN)(yN)\forall x, y \in N: (x \in N') \Leftrightarrow (y \in N')

so that, putting y=0:1Ny = 0: 1 \to N', we conclude that xNxNx \in N \Rightarrow x \in N', i.e., that NN' is all of NN.

Remark

A slightly alternative proof of sufficiency uses the theory of well-founded coalgebras, as given here. If NN is a fixpoint of the functor F(X)=1+XF(X) = 1+X, regarded as an FF-coalgebra, then the internal union of well-founded subcoalgebras of NN is a natural numbers object \mathbb{N}. Then the subobject N\mathbb{N} \hookrightarrow N can also be regarded as a subalgebra; by the lemma, it is all of NN. Thus NN is a natural numbers object.

Free constructions in a topos

In topos theory the existence of a natural numbers object (NNO) has a couple of far-reaching consequences.

Firstly, the existence of a NNO in a topos 𝒮\mathcal{S} is equivalent to the existence of free unary systems in 𝒮\mathcal{S}, unary systems being objects with an endomorphism in 𝒮\mathcal{S}.

Proposition

Let 𝒮\mathcal{S} be a topos and unsys(𝒮)\mathbf{unsys}(\mathcal{S}) its category of internal unary systems. Then 𝒮\mathcal{S} has a NNO precisely if the forgetful functor U:unsys(𝒮)𝒮U:\mathbf{unsys}(\mathcal{S})\to \mathcal{S} has a left adjoint.

Let F:𝒮unsys(𝒮)F:\mathcal{S}\to\mathbf{unsys}(\mathcal{S}) be a left adjoint to the forgetful functor UU, and let 11 be a terminal object in 𝒮\mathcal{S}. Then F(1)F(1) is a NNO in 𝒮\mathcal{S}, by definition of an NNO.

Secondly, it is a theorem due to C. J. Mikkelsen that the existence of a NNO in a topos 𝒮\mathcal{S} is equivalent to the existence of free monoids in 𝒮\mathcal{S}:

Proposition

Let 𝒮\mathcal{S} be a topos and mon(𝒮)\mathbf{mon}(\mathcal{S}) its category of internal monoids. Then 𝒮\mathcal{S} has a NNO precisely if the forgetful functor U:mon(𝒮)𝒮U:\mathbf{mon}(\mathcal{S})\to \mathcal{S} has a left adjoint.

For a proof see Johnstone (1977,p.190).

It then is a theorem due to Andreas Blass (1989) that 𝒮\mathcal{S} has a NNO precisely if 𝒮\mathcal{S} has an object classifier 𝒮[𝕆]\mathcal{S}[\mathbb{O}].

A consequence of this, discussed in sec. B4.2 of (Johnstone 2002,I p.431), is that classifying toposes for geometric theories over 𝒮\mathcal{S} exist precisely if 𝒮\mathcal{S} has a NNO.

So from a different perspective, in a topos the existence of free objects over various gadgets like e.g. algebraic theories or geometric theories (often) hinge on the existence of free unary systems or monoids, the intuition being that the free unary systems and free monoids permit to construct a free model syntactically by providing for the (syntactic) building blocks needed for this process.

Notice that algebraic theories can nevertheless have free algebras even if the ambient topos lacks a NNO. This may happen for algebraic theories that have the property that the free algebra on a finite set of generators has a finite carrier e.g. in the topos FinSetFinSet of finite sets free graphic monoids exist.

Examples

There are many examples of natural numbers objects.

In closed symmetric monoidal categories

Example

The natural numbers are the natural numbers object in the closed symmetric monoidal category Set.

Example

In classical mathematics, the extended natural numbers ¯=+{}\overline{\mathbb{N}} = \mathbb{N} + \{\infty\} are the natural numbers object in the closed symmetric monoidal category of pointed sets Set *Set_*, with z:𝟚¯z:\mathbb{2} \to \overline{\mathbb{N}} taking the boolean true to \infty and false to 00 and s:¯¯s:\overline{\mathbb{N}} \to \overline{\mathbb{N}} taking natural numbers to its successor and \infty to \infty. In constructive mathematics, the extended natural numbers ¯\overline{\mathbb{N}} and the disjoint union +{}\mathbb{N} + \{\infty\} are no longer the same; it is +{}\mathbb{N} + \{\infty\} which remains the natural numbers object in Set *Set_*.

Example

The underlying abelian group of the polynomial ring [X]\mathbb{Z}[X] is the natural numbers object in the closed symmetric monoidal category Ab, with z:[X]z:\mathbb{Z} \to \mathbb{Z}[X] taking integers to constant polynomials and s:[X][X]s:\mathbb{Z}[X] \to \mathbb{Z}[X] multiplying polynomials by the indeterminant XX.

Example

More generally, given a commutative ring RR, the underlying RR-module of the polynomial ring R[X]R[X] is the natural numbers object in the closed symmetric monoidal category RMod, with z:RR[X]z:R \to R[X] taking scalars to constant polynomials and s:R[X]R[X]s:R[X] \to R[X] multiplying polynomials by the indeterminant XX.

In a sheaf topos

In any Grothendieck topos E=Sh(C)E = Sh(C) the natural numbers object is given by the constant sheaf on the set of ordinary natural numbers, i.e. by the sheafification of the presheaf C opSetC^{op} \to Set that is constant on the set \mathbb{N}.

There are interesting cases in which such sheaf toposes contain objects that look like they ought to be natural numbers objects but do not satisfy the above axioms: for instance some of the models described at Models for Smooth Infinitesimal Analysis are sheaf toposes that contain besides the standard natural number object a larger object of smooth natural numbers that has generalized elements which are “infinite natural numbers” in the sense of nonstandard analysis.

Properties

Transfer along inverse images

Proposition

Natural number objects are preserved by inverse images:

let f=(f *f *):f *f *f = (f^* \dashv f_*) : \mathcal{E} \underoverset{f_*}{f^*}{\leftrightarrows} \mathcal{F} be a geometric morphism of toposes. If \mathbb{N} \in \mathcal{F} is a natural numbers object, then its inverse image f *f^* \mathbb{N} is a natural numbers object in \mathcal{E}.

(Johnstone, lemma A.4.1.14). Of course, by the finite colimit characterization, we need only the fact that inverse images preserve finite colimits and the terminal object.

Example

If \mathcal{E} is a sheaf topos, then there is a unique geometric morphism (ΔΓ):ΓΔSet(\Delta \dashv \Gamma): \mathcal{E} \underoverset{\Gamma}{\Delta}{\leftrightarrows} Set, the global section geometric morphism, with the inverse image being the locally constant sheaf functor, it follows that

Δ()Δ( n:1) n:NΔ1 n:1, \Delta(\mathbb{N}) \cong \Delta\left(\sum_{n: \mathbb{N}} 1\right) \cong \sum_{n: N} \Delta 1 \cong \sum_{n: \mathbb{N}} 1,

with the evident successor and constant 00, is the natural nunbers object in \mathcal{E}.

Example

If \mathcal{E} is a topos and XX \in \mathcal{E} an object, then the slice topos sits by an etale geometric morphism over \mathcal{E}

/XX *X *, \mathcal{E}_{/X} \stackrel{\overset{X^*}{\leftarrow}}{\underset{X_*}{\to}} \mathcal{E} \,,

where the inverse image form the product with XX. Hence for \mathbb{N} \in \mathcal{E} a natural numbers object, the projection (X×X)(X \times \mathbb{N} \to X) is a natural numbers object in /X\mathcal{E}_{/X}.

Relation to rig objects

The initial rig object in a category with finite products, (,0:1,1:1,+:×,×:×)\mathbb{N},0:1\rightarrow\mathbb{N},1:1\rightarrow\mathbb{N},+:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N},\times:\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}) with suitable commutative diagrams expressing the rig axioms and initiality, has the structure of a natural numbers object given by the triple (,0:1,x+1:)(\mathbb{N}, 0:1\rightarrow\mathbb{N}, x+1:\mathbb{N}\rightarrow\mathbb{N}).

Relation to object of integers

Given a natural numbers object \mathbb{N} in a pretopos, we can construct an integers object as follows. Let a,b:E×a, b\colon E \to \mathbb{N} \times \mathbb{N} be the kernel pair of the addition map +:×{+}\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N}, and let π 1,π 2:×\pi_1, \pi_2\colon \mathbb{N} \times \mathbb{N} \to \mathbb{N} be the product projections. We define \mathbb{Z} to be the coequalizer of the congruence (π 1a,π 2b),(π 1b,π 2a):E×(\pi_1 \circ a, \pi_2 \circ b), (\pi_1 \circ b, \pi_2 \circ a)\colon E \to \mathbb{N} \times \mathbb{N}. A similar construction yields a rational numbers object \mathbb{Q}.

For a real numbers object, rather more care is needed; see real numbers object.

References

Natural numbers as a classifying object for dinatural numbers:

In monoidal categories:

In elementary ( , 1 ) (\infty,1) -toposes:

Last revised on July 18, 2024 at 13:28:02. See the history of this page for a list of all contributions to it.